Nuprl Definition : f-rank 11,40
f-rank{i:l}
f-rank(x; free; es; e)
== if x changed before e
== then let r = f-rank{i:l}
== then let r = f-rank(x; free; es; (last change to x before e)) in
== then let rif eq_id(es-after(es; x; e); free) then inc-fst(r) else inc-snd(r) fi 
== else <0, 1>
== fi 

clarification:

f-rank{i:l}
f-rank(x; free; es; e)
== if changed{i:l}
== if changed(Id; id-deq; es; x; e)
== then let r = f-rank{i:l}
== then let r = f-rank(x; free; es; last-change{i:l}(Id; id-deq; es; x; e)) in
== then let rif eq_id(es-after(es; x; e); free) then inc-fst(r) else inc-snd(r) fi 
== else <0, 1>
== fi 
(recursive) 
latex

DefinitionsY, x.A(x), x changed before e, let x = a in b(x), f(a), (last change to x before e), Id, id-deq, if b then t else f fi , eq_id(a; b), es-after(es; x; e), inc-fst(p), inc-snd(p), <a, b>, #$n
FDL editor aliasesf-rank

origin